Nuprl Definition : weakPrecondSendR
11,40
postcript
pdf
at src(
l
):
action $a(m)
precondition
P
p
sends [$tg,
f
] on link
l
==
([Rpre(source(
l
);
ds
;"$a";
p
;
P
);
==
([
Rsends(
ds
;locl("$a");Outcome;
l
;"$tg" :
T
;[<"$tg",
s
,
v
. [(
f
(
s
,
v
))]>]);
==
([
Rsframe(
l
;"$tg";[locl("$a")])])
latex
clarification:
weakPrecondSendR{$a,$tg}(
T
;
p
;
l
;
ds
;
P
;
f
)
==
([Rpre(source(
l
);
ds
;"$a";
p
;
P
);
==
([
Rsends(
ds
;locl("$a");p-outcome(
p
);
l
;"$tg" :
T
;[<"$tg",
s
,
v
. [(
f
(
s
,
v
)) / []]> / []]) /
==
([
[Rsframe(
l
;"$tg";[locl("$a") / []]) / []]])
latex
Definitions
(
L
)
,
Rpre(
loc
;
ds
;
a
;
p
;
P
)
,
source(
l
)
,
Rsends(
ds
;
knd
;
T
;
l
;
dt
;
g
)
,
Outcome
,
x
:
v
,
<
a
,
b
>
,
x
.
A
(
x
)
,
f
(
a
)
,
Rsframe(
lnk
;
tag
;
L
)
,
[
car
/
cdr
]
,
locl(
a
)
,
"$x"
,
[]
FDL editor aliases
weakPrecondSendR
origin